Fiche membre Retour à l'annuaire
Gaétan GILBERT
IATOSS
: Gaetan.Gilbertatls2n.fr
Adresse :
Université de Nantes - faculté des Sciences et Techniques ( FST )Petit Port2 Chemin de la HoussinièreBP 92208
44322 Nantes Cedex 3
Publications référencées sur HAL
Revues internationales avec comité de lecture (ART_INT)
- [1] T. Zimmermann, J. Coolen, J. Gross, P. Pédrot, G. Gilbert. The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report. In IEEE Software ; éd. Institute of Electrical and Electronics Engineers, 2022.https://inria.hal.science/hal-03479327v2
- [2] G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau. Definitional Proof-Irrelevance without K. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2019.https://inria.hal.science/hal-01859964v2
- [3] Y. Leray, G. Gilbert, N. Tabareau, T. Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In International Conference on Interactive Theorem Proving (ITP 2024), septembre 2024, Tbilisi, Géorgie.https://inria.hal.science/hal-04511667v2
- [4] G. Gilbert, P. Pédrot, M. Sozeau, N. Tabareau. From Lost to the River: Embracing Sort Proliferation. In TYPES 2023 - 29th International Conference on Types for Proofs and Programs, juin 2023, Valencia, Espagne.https://inria.hal.science/hal-04378939v1
- [5] G. Gilbert, Y. Leray, N. Tabareau, T. Winterhalter. The Rewster: The Coq Proof Assistant with Rewrite Rules. In TYPES 2023 - 29th International Conference on Types for Proofs and Programs, juin 2023, Valencia, Espagne.https://inria.hal.science/hal-04403667v1
- [6] G. Gilbert. Formalising Real Numbers in Homotopy Type Theory. In 6th ACM SIGPLAN Conference on Certified Programs and Proofs, janvier 2017, Paris, France.https://inria.hal.science/hal-01449326v1
- [7] G. Gilbert, O. Hermant. Normalization by Completeness with Heyting Algebras. In LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, novembre 2015, Suva, Fidji.https://minesparis-psl.hal.science/hal-01204599v1
